随着我国铁路的迅速发展，对列车运行安全性的要求越来越高。采用Event-B形式化建模方法研究了高速列车安全距离控制形式化验证问题，以Event-B形式化仿真工具Rodin为基础，通过结合多智能体理论，引入感知决策法则，实现了无线闭塞中心(RBC)与列车的车地通信，建立了多列车运行的安全距离控制模型。仿真研究了高速列车最小间隔追踪控制运行，对列车安全距离控车行为进行了形式化建模并进行了POs证明义务验证。仿真结果表明，对于CTCS列车控制系统的复杂逻辑关联行为，采用提出的Event-B和多智能体系统(MAS)结合的形式化验证方法，可进行系统规范的模型验证，对于复杂系统的逻辑验证有较强的实际意义。
